$M$.ef($k$,$x$,$s$,$v$)?$w$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}cap(($M$.2.2.2.2).1;product{-}deq(Knd;Id;KindDeq;IdDeq);$<$$k$, $x$$>$;$\lambda$$s$,$v$. $w$)($s$,$v$)